FDL - Nuprl Lemma : max-of-intset

Nuprl Lemma : max-of-intset

P:(

).
(

n:

. Dec(P(n)))

(

n:

.

(

y:

. (y

n)

(

P(y)))

(

y:

. ((y

n) & P(y) & (

x:

. ((y < x) & (x

n))

(

P(x))))))

Definitions SQType(T), {T}, , i j , False, A, A B, P Q, t T, P & Q, x:A. B(x), x(s), P Q, , x:A. B(x), Dec(P)

Lemmas not wf, le wf, ge wf, nat properties, decidable wf, nat wf